$\forall$$X$:Type, ${\it eq}$:EqDecider($X$), $f$, $g$:$x$:$X$ fp$\rightarrow$ Type, $x$:$X$, $z$:$g$($x$)?Void.
\\[0ex]$f$ $\parallel$ $g$ $\Rightarrow$ ($f$($x$)?Void $\subseteq$r $g$($x$)?Void)